Inference at * 2 1 1 1 2 1 1 
Iof proof for Lemma fseg select:



1. T : Type
2. l1 : T List
3. l2 : T List
4. ||l1||  ||l2||
5. i:. (i < ||l1||)  (l1[i] = l2[((||l2|| - ||l1||)+i)])
6. i : 
7. i < ||l1||
8. l1[i] = l2[((||l2|| - ||l1||)+i)]
  l1[i] = l2[(i+(||l2|| - ||l1||))] 

latex

 by ParallelOp (-1) 

latex

 .

Definitions	SQType(T), {T}, s ~ t, {x:A| B(x)} , i  j , T, True, A, False, -n, , P & Q, x:A  B(x), , l[i], P  Q, t  T, #$n, n+m, n - m, ||as||, s = t, , x:A. B(x), x:AB(x), A  B, type List, Type, a < b
Lemmas	guard wf, le wf, squash wf, select wf